Tennent's Correspondence Principle and Returning From a Closure

I just had a very productive meeting with coauthors of the closure proposal. I think we made a lot of progress addressing most of the specific concerns people have with the proposal (with the exception of subjective comments like "I don't think you should do this kind of thing to Java").

One issue in particular has been nagging us, and in spite of Gilad's insistence that we comply with Tennent's Correspondence and Abstraction Principles (described in detail in the now out-of-print book Principles of Programming Languages by R.D.Tennent), Gilad reluctantly admitted before we published the first draft that there doesn't seem to be a way of doing that for returning from a closure without introducing inconsistencies with the rest of the language. In the end we discovered that there is indeed a way to do it, and it seems to be rather cleaner than any of the alternatives.

Setting aside the technical details of Tennent's approach, the principle applies directly to the closure construct. A closure can be used to abstract over an expression or a statement. The principle dictates that an expression or statement, when wrapped in a closure and then immediately invoked, ought to have the same meaning as it did before being wrapped in a closure. Any change in semantics when wrapping code in a closure is likely a flaw in the language.

To put this more concretely, an expression

expr

should have the same meaning as the expression that wraps it in a closure and then evaluates it:

(():expr}()

And a block statement

{ stmt; ... }

ought to have the same meaning as creating and invoking a closure that wraps the statement:

((){ stmt; ... })()

Tennent's principles are very powerful because violations of them tend to show up in the language as flaws, irregularities, unnecessary restrictions, unexpected interactions or complications, and so on. While exploring the language design space for closures, every time we were tempted to violate them we found that there were very real and unpleasant consequences; they are very powerful tools for detecting bad smells in a programming language design. The principles apply no less when extending an existing programming language, because what you are doing in that case is designing the next version of a language. We discovered that when a bad smell is detected by these principles, it is often straightforward to illustrate specific problems. The problems we identified also arise in many supposedly "simpler" proposals that attempt to provide merely a shorthand notation for construcing anonymous class instances. I'll show two specific issues that we identified based on bad smells, examples of the real problems caused, and how we solved them.

The meaning of this

Before we look at the question of how to return from a closure, and to help understand how the principles are applied, let's look at the application of Tennent's principles to the question of the meaning of this within a closure. One possibility would be that it designates the closure object itself. That might be useful if you want to define a recursive closure, as you now have a convenient way of invoking yourself. An alternative is that it designates the anonymous class instance that is created if the closure conversion is applied. That seems natural if you like to think of the closure expression as a shorthand for creating an anonymous class.

Unfortunately, both of these alternatives get you into trouble, and we can show specific ways that the language no longer fits together when you take these approaches. The former approach, for example, doesn't allow you to analyze the types of expressions appearing within the closure, because the closure type depends on the type of the returned expression, but the returned expression might use "this", and so may depend on the type of the closure. The latter approach has a similar chicken-and-egg problem, because the type of interface you're creating may depend on the types within the closure, but the types within the closure depend on the type of the interface you're creating.

To see the problem more simply, one issue is that the expression this no longer designates the same thing when wrapped by a closure. In order to abstract (i.e., wrap a closure around) a piece of code that uses this or uses any names that are inherited from Object, you would have to systematically rewrite those names to qualify them in some way to ensure that they refer to the appropriate object. In other words, you'd have to change every this to EnclosingClassName.this and every toString() to EnclosingClassName.this.toString(). To be most useful as an abstraction facility, programmers should be free to wrap a piece of code in a closure without worrying that its semantics will change subtly. To satisfy Tennent's Correspondence Principle, a closure should introduce into the scope of the closure no names that are not explicitly declared by the user - that is, only the closure's parameters.

Returning from a closure

The principle also applies to the problem of returning from a closure. The current draft proposal suggests that we use the existing return syntax for returning from a closure, but that violates the principles; you can detect the bad smell by observing that this statement

{ if (...) return; }

doesn't mean the same thing as this:

(){ if (...) return; } ()

The former returns to the enclosing method (not shown), while the latter returns from the closure, effectively doing nothing.

One idea, desribed in the further ideas section of the draft spec, is to introduce a new syntax for returning from a closure, and reserve the return statement for returning from a method, function, or constructor. We toyed with the statement syntax

^ expression;

Setting aside aesthetics, this seems to satisfy the requirements, because this isn't legal syntax outside a closure. Existing code does not have statements of this form, so wrapping such code could not change its meaning. However, on further reflection we realized that this syntax and all of the other new kinds of return statements that we considered have the same flaw as using return: while existing code doesn't use this new statement form, once we introduce it into the language we should expect people to start using it in new code. And once they do, any code that includes this statement cannot be wrapped in a closure without changing its meaning. Once we identified the bad smell this way, it wasn't hard to come up with realistic examples where it gets in the way of using the language.

Having eliminated any form of return statement, what are you left with? Referring back to Tennent's principles is instructive: you should be able to replace an expression expr with

(){ expr } ()

This is the proposed syntax for returning a value from a closure. It is simpler than the existing spec because no rules are needed to infer the return type; it is the type of the expression. Of course, we will want to allow a list of statements instead of an expression to allow the construct to close over statements (in which case the closure returns void), and allow a list of statements to precede a trailing expression (in which case the final expression is the result of the closure). An expression without a trailing semicolon isn't a legal statement form, so there is no confusion with any existing constructs. This nicely satisfies Tennent's principles. My only regret is that there is no single way to both designate the returned value and return from a closure before its end, which would be slightly more consistent with Java's existing control constructs.

And more...

We made progress on a number of issues:

• We know how to address concerns about how the closure conversion will interact with APIs like concurrency and asynchronous notification systems where the closure isn't just called by the current thread; in those APIs you don't want to allow nonlocal control-flow or capturing nonfinal variables.
• We think we can add support for type inference of exception types to allow writing APIs in which the set of exceptions from a block (closure) that is passed in to the API can propogate out of the API while being strongly type-checked.
• We think it should be possible to write a class that "implements" a function type, as suggested by "crazy" Bob Lee, so that you can define a custom toString() to make debugging easier or make the implementation serializable.
• We started looking at a number of specific use cases that have been suggested, such as a library that allows you to execute a block of code while holding a java.util.concurrent.locks.Lock, unlocking it at the end, or a library that closes your streams (or other Closable things) after your block of code is finished.
• We've also made progress on detailing the set of implementation techniques that might be used to implement the facility.

I'll blog about these later.